Search for: All records

Symbolic execution is a powerful program analysis and testing technique. Symbolic execution engines are usually implemented as interpreters, and the induced interpretation over-head can dramatically inhibit performance. Alternatively, implementation choices based on instrumentation provide a limited ability to transform programs. However, the use of compilation and code generation techniques beyond simple instrumentation remains underexplored for engine construction, leaving potential performance gains untapped. In this paper, we show how to tap some of these gains using sophisticated compilation techniques: We present Gensym, an optimizing symbolic-execution compiler that generates symbolic code which explores paths and generates tests in parallel. The key insight of GensYmis to compile symbolic execution tasks into cooperative concurrency via continuation-passing style, which further enables efficient parallelism. The design and implementation of Gensym is based on partial evaluation and generative programming techniques, which make it high-level and performant at the same time. We compare the performance of Gensym against the prior symbolic-execution compiler LLSC and the state-of-the-art symbolic interpreter KLEE. The results show an average 4.6× speedup for sequential execution and 9.4× speedup for parallel execution on 20 benchmark programs. 

We present the demonstration of CEIVE (Callee-only inference and verification), an effective and practical defense against caller ID spoofing. CEIVE is a victim callee only solution without requiring additional infrastructure support or changes on telephony systems; It is ready to deploy and easy to use. Given an incoming call, CEIVE leverages a callback session and its associated call signaling observed at the phone to infer the call state of the other party. It further compares with the anticipated call state of the incoming call, thus quickly verifying whether the incoming call comes from the originating number or not. In this demo, we demonstrate CEIVE installed on Android phones combating both basic and advanced caller ID spoofing attacks. 

Caller ID spoofing forges the authentic caller identity, thus making the call appear to originate from another user. This seemingly simple attack technique has been used in the growing telephony frauds and scam calls, resulting in substantial monetary loss and victim complaints. Unfortunately, caller ID spoofing is easy to launch, yet hard to defend; no effective and practical defense solutions are in place to date. In this paper, we propose CEIVE (Callee-only inference and verification), an effective and practical defense against caller ID spoofing. It is a victim callee only solution without requiring additional infrastructure support or changes on telephony systems. We formulate the design as an inference and verification problem. Given an incoming call, CEIVE leverages a callback session and its associated call signaling observed at the phone to infer the call state of the other party. It further compares with the anticipated call state, thus quickly verifying whether the incoming call comes from the originating number. We exploit the standardized call signaling messages to extract useful features, and devise call-specific verification and learning to handle diversity and extensibility. We implement CEIVE on Android phones and test it with all top four US mobile carriers, one landline and two small carriers. It shows 100% accuracy in almost all tested spoofing scenarios except one special, targeted attack case.